$\forall$${\it ds}$:$z$:Id fp$\rightarrow$ Type. State(${\it ds}$) $\in$ Type